home *** CD-ROM | disk | FTP | other *** search
/ Language/OS - Multiplatform Resource Library / LANGUAGE OS.iso / lisp / eulisp / mpfeel.lha / MPFeel / Modules / boyer.em < prev    next >
Lisp/Scheme  |  1992-10-06  |  15KB  |  641 lines
  1. ;; $aclHeader: boyer.cl,v 1.3 90/10/16 11:59:14 layer Rel $
  2.  
  3. ;;; BOYER -- Logic programming benchmark, originally written by Bob Boyer.
  4. ;;; Fairly CONS intensive.
  5.  
  6. (defmodule boyer
  7.   ((except (memq member assoc) 
  8.        (rename ((car rcar) (cdr rcdr))
  9.            standard0))
  10.    futures 
  11.    plists)
  12.   ()
  13.   
  14.   (defun assoc (a l p)
  15.     (cond ((null (future-value l)) nil)
  16.       ((p (future-value a) (car (car l)))
  17.        (car l))
  18.       (t (assoc a (cdr l) p))))
  19.  
  20.   (defun memq (a l)
  21.     (cond ((null l) nil)
  22.       ((eq a (car l)))
  23.       (t (memq a (cdr l)))))
  24.  
  25.   (defun member (a l p)
  26.     (cond ((null (future-value l)) nil)
  27.       ((p a (car l)))
  28.       (t (member a (cdr l) p))))
  29.  
  30.   (defun add-lemma (term)
  31.     (cond ((and (not (atom term))
  32.         (eq (car term)
  33.             (quote equal))
  34.         (not (atom (cadr term))))
  35.        ((setter get) (caadr term) (quote lemmas)
  36.         (cons term (get (caadr term) (quote lemmas)))))
  37.       (t (error "~%ADD-LEMMA did not like term:  ~a" term))))
  38.  
  39.   (defmethod equal ((x future-object) y)
  40.     (equal (future-value x) (future-value y)))
  41.  
  42.   (defmethod equal (x (y future-object))
  43.     (equal (future-value x) (future-value y)))
  44.  
  45.   (defun add-lemma-lst (lst)
  46.     (cond ((null lst)
  47.        t)
  48.       (t (add-lemma (car lst))
  49.          (add-lemma-lst (cdr lst)))))
  50.  
  51.   (defgeneric car (x))
  52.   (defmethod car ((x pair))
  53.     (rcar x))
  54.   
  55.   (defmethod car ((x future-object))
  56.     (rcar (future-value x)))
  57.   
  58.   (defgeneric cdr (x))
  59.  
  60.   (defmethod cdr ((x pair))
  61.     (rcdr x))
  62.   
  63.   (defmethod cdr ((x future-object))
  64.     (rcdr (future-value x)))
  65.   
  66.   ((setter setter) car (setter rcar))
  67.  
  68.   (defun apply-subst (alist term)
  69.     (let ((**temp-temp** nil))
  70.       (cond ((atom term)
  71.          (cond ((setq **temp-temp** (assoc term alist eq))
  72.             (cdr **temp-temp**))
  73.            (t term)))
  74.         (t (cons (car term)
  75.              (apply-subst-lst alist (cdr term)))))))
  76.  
  77.   (defun apply-subst-lst (alist lst)
  78.     (cond ((null lst)
  79.        nil)
  80.       (t (cons (apply-subst alist (car lst))
  81.            (apply-subst-lst alist (cdr lst))))))
  82.  
  83.   (defun falsep (x lst)
  84.     (or (equal x (quote (f)))
  85.     (member x lst equal)))
  86.  
  87.   (defun one-way-unify (term1 term2 **unify-subst**)
  88.     (progn ((setter car) **unify-subst** nil)
  89.        (one-way-unify1 term1 term2 **unify-subst**)))
  90.  
  91.   (defun one-way-unify1 (term1 term2 **unify-subst**)
  92.     ;;(format t "Unify: ~a ~a~%" term1 term2)
  93.     (let ((**temp-temp** nil))
  94.       (let ((term2a (future-value term2)))
  95.     (cond ((atom term2a)
  96.            (cond ((setq **temp-temp** (assoc term2a (car **unify-subst**) eq))
  97.               (equal term1 (cdr **temp-temp**)))
  98.              (t ((setter car) **unify-subst** (cons (cons term2a term1)
  99.                                 (car **unify-subst**)))
  100.             t)))
  101.           ((atom (future-value term1))
  102.            nil)
  103.           ((eq (future-value (car term1))
  104.            (future-value (car term2a)))
  105.            (one-way-unify1-&lst (cdr term1)
  106.                     (cdr term2a)
  107.                     **unify-subst**))
  108.           (t nil)))))
  109.  
  110.   (defun one-way-unify1-&lst (lst1 lst2 **unify-subst**)
  111.     (cond ((null lst1)
  112.        t)
  113.       ((one-way-unify1 (car lst1)
  114.                (car lst2)
  115.                            **unify-subst**)
  116.        (one-way-unify1-&lst (cdr lst1)
  117.                 (cdr lst2)
  118.                 **unify-subst**))
  119.       (t nil)))
  120.  
  121.   (defun rewrite (term)
  122.     (cond ((atom term)
  123.        term)
  124.       (t (rewrite-with-lemmas (cons (car term)
  125.                     (rewrite-args (cdr term)))
  126.                   (get (car term)
  127.                        (quote lemmas))))))
  128.  
  129.   (defun rewrite-args (lst)
  130.     (cond ((null lst)
  131.        nil)
  132.       (t (cons (future (rewrite (car lst)))
  133.            (rewrite-args (cdr lst))))))
  134.  
  135.   (defun rewrite-with-lemmas (term lst)
  136.     (let ((**unify-subst** (cons nil nil)))
  137.       (cond ((null lst)
  138.          term)
  139.         ((one-way-unify term (cadr (car lst)) **unify-subst**)
  140.          (rewrite (apply-subst (car **unify-subst**) (caddr (car lst)))))
  141.         (t (rewrite-with-lemmas term (cdr lst))))))
  142.  
  143.   (defun boyer-setup ()
  144.     (add-lemma-lst
  145.      (quote ((equal (compile form)
  146.             (reverse (codegen (optimize form)
  147.                       (nil))))
  148.          (equal (eqp x y)
  149.             (equal (fix x)
  150.                (fix y)))
  151.          (equal (greaterp x y)
  152.             (lessp y x))
  153.          (equal (lesseqp x y)
  154.             (not (lessp y x)))
  155.          (equal (greatereqp x y)
  156.             (not (lessp x y)))
  157.          (equal (boolean x)
  158.             (or (equal x (t))
  159.             (equal x (f))))
  160.          (equal (iff x y)
  161.             (and (implies x y)
  162.              (implies y x)))
  163.          (equal (even1 x)
  164.             (if (zerop x)
  165.             (t)
  166.               (odd (- x 1))))
  167.          (equal (countps- l pred)
  168.             (countps-loop l pred (zero)))
  169.          (equal (fact- i)
  170.             (fact-loop i 1))
  171.          (equal (reverse- x)
  172.             (reverse-loop x (nil)))
  173.          (equal (divides x y)
  174.             (zerop (remainder y x)))
  175.          (equal (assume-true var alist)
  176.             (cons (cons var (t))
  177.               alist))
  178.          (equal (assume-false var alist)
  179.             (cons (cons var (f))
  180.               alist))
  181.          (equal (tautology-checker x)
  182.             (tautologyp (normalize x)
  183.                 (nil)))
  184.          (equal (falsify x)
  185.             (falsify1 (normalize x)
  186.                   (nil)))
  187.          (equal (prime x)
  188.             (and (not (zerop x))
  189.              (not (equal x (add1 (zero))))
  190.              (prime1 x (- x 1))))
  191.          (equal (and p q)
  192.             (if p (if q (t)
  193.                 (f))
  194.               (f)))
  195.          (equal (or p q)
  196.             (if p (t)
  197.               (if q (t)
  198.             (f))
  199.               (f)))
  200.          (equal (not p)
  201.             (if p (f)
  202.               (t)))
  203.          (equal (implies p q)
  204.             (if p (if q (t)
  205.                 (f))
  206.               (t)))
  207.          (equal (fix x)
  208.             (if (numberp x)
  209.             x
  210.               (zero)))
  211.          (equal (if (if a b c)
  212.             d e)
  213.             (if a (if b d e)
  214.               (if c d e)))
  215.          (equal (zerop x)
  216.             (or (equal x (zero))
  217.             (not (numberp x))))
  218.          (equal (plus (plus x y)
  219.               z)
  220.             (plus x (plus y z)))
  221.          (equal (equal (plus a b)
  222.                (zero))
  223.             (and (zerop a)
  224.              (zerop b)))
  225.          (equal (difference x x)
  226.             (zero))
  227.          (equal (equal (plus a b)
  228.                (plus a c))
  229.             (equal (fix b)
  230.                (fix c)))
  231.          (equal (equal (zero)
  232.                (difference x y))
  233.             (not (lessp y x)))
  234.          (equal (equal x (difference x y))
  235.             (and (numberp x)
  236.              (or (equal x (zero))
  237.                  (zerop y))))
  238.          (equal (meaning (plus-tree (append x y))
  239.                  a)
  240.             (plus (meaning (plus-tree x)
  241.                    a)
  242.               (meaning (plus-tree y)
  243.                    a)))
  244.          (equal (meaning (plus-tree (plus-fringe x))
  245.                  a)
  246.             (fix (meaning x a)))
  247.          (equal (append (append x y)
  248.                 z)
  249.             (append x (append y z)))
  250.          (equal (reverse (append a b))
  251.             (append (reverse b)
  252.                 (reverse a)))
  253.          (equal (times x (plus y z))
  254.             (plus (times x y)
  255.               (times x z)))
  256.          (equal (times (times x y)
  257.                z)
  258.             (times x (times y z)))
  259.          (equal (equal (times x y)
  260.                (zero))
  261.             (or (zerop x)
  262.             (zerop y)))
  263.          (equal (exec (append x y)
  264.               pds envrn)
  265.             (exec y (exec x pds envrn)
  266.               envrn))
  267.          (equal (mc-flatten x y)
  268.             (append (flatten x)
  269.                 y))
  270.          (equal (member x (append a b))
  271.             (or (member x a)
  272.             (member x b)))
  273.          (equal (member x (reverse y))
  274.             (member x y))
  275.          (equal (length (reverse x))
  276.             (length x))
  277.          (equal (member a (intersect b c))
  278.             (and (member a b)
  279.              (member a c)))
  280.          (equal (nth (zero)
  281.              i)
  282.             (zero))
  283.          (equal (exp i (plus j k))
  284.             (times (exp i j)
  285.                (exp i k)))
  286.          (equal (exp i (times j k))
  287.             (exp (exp i j)
  288.              k))
  289.          (equal (reverse-loop x y)
  290.             (append (reverse x)
  291.                 y))
  292.          (equal (reverse-loop x (nil))
  293.             (reverse x))
  294.          (equal (count-list z (sort-lp x y))
  295.             (plus (count-list z x)
  296.               (count-list z y)))
  297.          (equal (equal (append a b)
  298.                (append a c))
  299.             (equal b c))
  300.          (equal (plus (remainder x y)
  301.               (times y (quotient x y)))
  302.             (fix x))
  303.          (equal (power-eval (big-plus1 l i base)
  304.                 base)
  305.             (plus (power-eval l base)
  306.               i))
  307.          (equal (power-eval (big-plus x y i base)
  308.                 base)
  309.             (plus i (plus (power-eval x base)
  310.                   (power-eval y base))))
  311.          (equal (remainder y 1)
  312.             (zero))
  313.          (equal (lessp (remainder x y)
  314.                y)
  315.             (not (zerop y)))
  316.          (equal (remainder x x)
  317.             (zero))
  318.          (equal (lessp (quotient i j)
  319.                i)
  320.             (and (not (zerop i))
  321.              (or (zerop j)
  322.                  (not (equal j 1)))))
  323.          (equal (lessp (remainder x y)
  324.                x)
  325.             (and (not (zerop y))
  326.              (not (zerop x))
  327.              (not (lessp x y))))
  328.          (equal (power-eval (power-rep i base)
  329.                 base)
  330.             (fix i))
  331.          (equal (power-eval (big-plus (power-rep i base)
  332.                       (power-rep j base)
  333.                       (zero)
  334.                       base)
  335.                 base)
  336.             (plus i j))
  337.          (equal (gcd x y)
  338.             (gcd y x))
  339.          (equal (nth (append a b)
  340.              i)
  341.             (append (nth a i)
  342.                 (nth b (difference i (length a)))))
  343.          (equal (difference (plus x y)
  344.                 x)
  345.             (fix y))
  346.          (equal (difference (plus y x)
  347.                 x)
  348.             (fix y))
  349.          (equal (difference (plus x y)
  350.                 (plus x z))
  351.             (difference y z))
  352.          (equal (times x (difference c w))
  353.             (difference (times c x)
  354.                 (times w x)))
  355.          (equal (remainder (times x z)
  356.                    z)
  357.             (zero))
  358.          (equal (difference (plus b (plus a c))
  359.                 a)
  360.             (plus b c))
  361.          (equal (difference (add1 (plus y z))
  362.                 z)
  363.             (add1 y))
  364.          (equal (lessp (plus x y)
  365.                (plus x z))
  366.             (lessp y z))
  367.          (equal (lessp (times x z)
  368.                (times y z))
  369.             (and (not (zerop z))
  370.              (lessp x y)))
  371.          (equal (lessp y (plus x y))
  372.             (not (zerop x)))
  373.          (equal (gcd (times x z)
  374.              (times y z))
  375.             (times z (gcd x y)))
  376.          (equal (value (normalize x)
  377.                a)
  378.             (value x a))
  379.          (equal (equal (flatten x)
  380.                (cons y (nil)))
  381.             (and (nlistp x)
  382.              (equal x y)))
  383.          (equal (listp (gopher x))
  384.             (listp x))
  385.          (equal (samefringe x y)
  386.             (equal (flatten x)
  387.                (flatten y)))
  388.          (equal (equal (greatest-factor x y)
  389.                (zero))
  390.             (and (or (zerop y)
  391.                  (equal y 1))
  392.              (equal x (zero))))
  393.          (equal (equal (greatest-factor x y)
  394.                1)
  395.             (equal x 1))
  396.          (equal (numberp (greatest-factor x y))
  397.             (not (and (or (zerop y)
  398.                   (equal y 1))
  399.                   (not (numberp x)))))
  400.          (equal (times-list (append x y))
  401.             (times (times-list x)
  402.                (times-list y)))
  403.          (equal (prime-list (append x y))
  404.             (and (prime-list x)
  405.              (prime-list y)))
  406.          (equal (equal z (times w z))
  407.             (and (numberp z)
  408.              (or (equal z (zero))
  409.                  (equal w 1))))
  410.          (equal (greatereqpr x y)
  411.             (not (lessp x y)))
  412.          (equal (equal x (times x y))
  413.             (or (equal x (zero))
  414.             (and (numberp x)
  415.                  (equal y 1))))
  416.          (equal (remainder (times y x)
  417.                    y)
  418.             (zero))
  419.          (equal (equal (times a b)
  420.                1)
  421.             (and (not (equal a (zero)))
  422.              (not (equal b (zero)))
  423.              (numberp a)
  424.              (numberp b)
  425.              (equal (- a 1)
  426.                 (zero))
  427.              (equal (- b 1)
  428.                 (zero))))
  429.          (equal (lessp (length (delete x l))
  430.                (length l))
  431.             (member x l))
  432.          (equal (sort2 (delete x l))
  433.             (delete x (sort2 l)))
  434.          (equal (dsort x)
  435.             (sort2 x))
  436.          (equal (length (cons x1
  437.                   (cons x2
  438.                     (cons x3 (cons x4
  439.                                (cons x5
  440.                                  (cons x6 x7)))))))
  441.             (plus 6 (length x7)))
  442.          (equal (difference (add1 (add1 x))
  443.                 2)
  444.             (fix x))
  445.          (equal (quotient (plus x (plus x y))
  446.                   2)
  447.             (plus x (quotient y 2)))
  448.          (equal (sigma (zero)
  449.                i)
  450.             (quotient (times i (add1 i))
  451.                   2))
  452.          (equal (plus x (add1 y))
  453.             (if (numberp y)
  454.             (add1 (plus x y))
  455.               (add1 x)))
  456.          (equal (equal (difference x y)
  457.                (difference z y))
  458.             (if (lessp x y)
  459.             (not (lessp y z))
  460.               (if (lessp z y)
  461.               (not (lessp y x))
  462.             (equal (fix x)
  463.                    (fix z)))))
  464.          (equal (meaning (plus-tree (delete x y))
  465.                  a)
  466.             (if (member x y)
  467.             (difference (meaning (plus-tree y)
  468.                          a)
  469.                     (meaning x a))
  470.               (meaning (plus-tree y)
  471.                    a)))
  472.          (equal (times x (add1 y))
  473.             (if (numberp y)
  474.             (plus x (times x y))
  475.               (fix x)))
  476.          (equal (nth (nil)
  477.              i)
  478.             (if (zerop i)
  479.             (nil)
  480.               (zero)))
  481.          (equal (last (append a b))
  482.             (if (listp b)
  483.             (last b)
  484.               (if (listp a)
  485.               (cons (car (last a))
  486.                 b)
  487.             b)))
  488.          (equal (equal (lessp x y)
  489.                z)
  490.             (if (lessp x y)
  491.             (equal t z)
  492.               (equal f z)))
  493.          (equal (assignment x (append a b))
  494.             (if (assignedp x a)
  495.             (assignment x a)
  496.               (assignment x b)))
  497.          (equal (car (gopher x))
  498.             (if (listp x)
  499.             (car (flatten x))
  500.               (zero)))
  501.          (equal (flatten (cdr (gopher x)))
  502.             (if (listp x)
  503.             (cdr (flatten x))
  504.               (cons (zero)
  505.                 (nil))))
  506.          (equal (quotient (times y x)
  507.                   y)
  508.             (if (zerop y)
  509.             (zero)
  510.               (fix x)))
  511.          (equal (get j (set i val mem))
  512.             (if (eqp j i)
  513.             val
  514.               (get j mem)))))))
  515.  
  516.   (defun tautologyp (x true-lst false-lst)
  517.     (cond ((truep x true-lst)
  518.        t)
  519.       ((falsep x false-lst)
  520.        nil)
  521.       ((atom (future-value x))
  522.        nil)
  523.       ((eq (future-value (car (future-value x)))
  524.            (quote if))
  525.        (cond ((truep (car (cdr x))
  526.              true-lst)
  527.           (tautologyp (car (cdr (cdr x)))
  528.                   true-lst false-lst))
  529.          ((falsep (car (cdr x))
  530.               false-lst)
  531.           (tautologyp (car (cdr (cdr (cdr x))))
  532.                   true-lst false-lst))
  533.          (t (and (tautologyp (car (cdr (cdr x)))
  534.                      (cons (car (cdr x))
  535.                        true-lst)
  536.                      false-lst)
  537.              (tautologyp (car (cdr (cdr (cdr x))))
  538.                      true-lst
  539.                      (cons (car (cdr x))
  540.                        false-lst))))))
  541.       (t nil)))
  542.  
  543.   (defun tautp (x)
  544.     (tautologyp (rewrite x)
  545.         nil nil))
  546.  
  547.   (defun boyer-test ()
  548.     (let ((term
  549.        (apply-subst
  550.         (quote ((x f (plus (plus a b)
  551.                    (plus c (zero))))
  552.             (y f (times (times a b)
  553.                 (plus c d)))
  554.             (z f (reverse (append (append a b)
  555.                       (nil))))
  556.             (u equal (plus a b)
  557.                (difference x y))
  558.             (w lessp (remainder a b)
  559.                (member a (length b)))))
  560.         (quote (implies (and (implies x y)
  561.                  (and (implies y z)
  562.                       (and (implies z u)
  563.                        (implies u w))))
  564.                 (implies x w))))))
  565.       (tautp term)))
  566.  
  567. (deflocal ans ())
  568.  
  569. (defun boyer-short-test ()
  570.   (let ((term
  571.      (apply-subst
  572.       (quote ((x f (plus (plus a b)
  573.                  (plus c (zero))))
  574.           (y f (times (times a b)
  575.                   (plus c d)))
  576.           (z f (reverse (append (append a b)
  577.                     (nil))))
  578.           (u equal (plus a b)
  579.              (difference x y))
  580.           (w lessp (remainder a b)
  581.              (member a (length b)))))
  582.       (quote (implies (and (implies x y)
  583.                    (and (implies z u)
  584.                     (implies u w)))
  585.               (implies x w))))))
  586.     (setq ans (tautp term))))
  587.  
  588. (defun boyer-very-short-test ()
  589.   (let ((term
  590.      (apply-subst
  591.       (quote ((x f (plus (plus a b)
  592.                  (plus c (zero))))
  593.           (y f (times (times a b)
  594.                   (plus c d)))
  595.           (z f (reverse (append (append a b)
  596.                     (nil))))
  597.           (u equal (plus a b)
  598.              (difference x y))
  599.           (w lessp (remainder a b)
  600.              (member a (length b)))))
  601.       (quote (implies x y)))))
  602.     (print term)
  603.     (setq ans (tautp term))))
  604.  
  605.   (defun trans-of-implies (n)
  606.     (list (quote implies)
  607.       (trans-of-implies1 n)
  608.       (list (quote implies)
  609.         0 n)))
  610.  
  611.   (defun trans-of-implies1 (n)
  612.     (cond ((= n 1)
  613.        (list (quote implies)        
  614.          0 1))
  615.       (t (list (quote and)
  616.            (list (quote implies)
  617.              (- n 1)
  618.              n)
  619.            (trans-of-implies1 (- n 1))))))
  620.  
  621.  
  622.   (defun truep (x lst)
  623.     (or (equal x (quote (t)))
  624.     (member x lst equal)))
  625.  
  626. (boyer-setup)
  627. ;;(defvar setup-performed-p t)
  628.  
  629.   (defun testboyer ()
  630.     (let ((xx (cpu-time)))
  631.       (print (boyer-test))
  632.       (- (cpu-time) xx)))
  633.  
  634.   (defun testshortboyer ()
  635.     (print (boyer-short-test)))
  636.  
  637.   (defun testveryshortboyer ()
  638.     (print (boyer-very-short-test)))
  639.  
  640. )                    ; end of module
  641.